$\vdash$  $\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{P}$), $f$:($\forall$$x$:$T$. Dec($P$($x$))). p{-}co{-}filter($f$) $\in$ $T$$\rightarrow$($T$ + Top)